ds1, ds1', ds2, ds2':a:Id fp Type, da, da':a:Knd fp Type.
ds1  ds1'  ds2'  ds2  da  da'  effect-type(ds1;ds2;da)  effect-type(ds1';ds2';da') 

latex

Definitions	{T}, KindDeq, f  g, IdDeq, effect-type(ds;ds';da), a:A fp B(a), (x  l), State(ds), 1of(t), Valtype(da;k), t  T, f(x)?z, Top, 2of(t), Knd, Id, x. t(x), x:A. B(x), P  Q
Lemmas	ma-valtype-subtype, fpf-cap wf, top wf, pi2 wf, subtype rel function, ma-state-subtype, ma-valtype wf, pi1 wf, subtype rel dep function, ma-state wf, l member wf, subtype rel product, Id wf, fpf wf, Knd wf, id-deq wf, fpf-sub wf, Kind-deq wf, subtype-fpf-cap